feat: Kani harnesses for scheduler + codegen invariants (#136)#141
Open
feat: Kani harnesses for scheduler + codegen invariants (#136)#141
Conversation
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
Adds bounded Kani proof harnesses for spar-solver and spar-codegen, each citing the Lean theorem it mirrors. spar-solver/tests/kani_solver.rs: - kani_schedule_implies_no_deadline_miss mirrors RMBound.lean:49 + 76 - kani_priority_monotonicity mirrors RTA.lean:74 + 65 - kani_zero_laxity_handled mirrors EDF.lean:88 + RMBound.lean:38 spar-codegen/tests/kani_codegen.rs: - kani_emit_preserves_schedule mirrors RTA.lean:186 All harnesses use #[kani::proof] + #[kani::unwind(8)] with MAX_TASKS=4. Production source unchanged. Kani-only deps gated behind `[target.'cfg(kani)'.dev-dependencies]`. Kani-cfg lint allowance added. CI: new `kani` job in ci.yml with `continue-on-error: true` while bounds are tuned. Comment in workflow describes hard-gate plan. Traceability in `artifacts/verification.yaml`: 4 VAL-KANI-* entries with `proof_link:` fields pointing to the Lean theorems. Closes #136. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
The actual Kani CI failure on this PR was a single unwinding-assertion
violation in `kani_emit_preserves_schedule`:
Check 275: emit.unwind.0
- Status: FAILURE
- Description: "unwinding assertion loop 0"
- Location: crates/spar-codegen/tests/kani_codegen.rs:86 (header iter)
All four `kani_zero_laxity_handled` assertions actually verified
SUCCESSFULLY (Checks 10-15) — those assertions are constructed
deterministically with `period=1000, wcet=500` so `total_util_ppm` is
exactly 1_000_000 by construction. The "Description" lines in CBMC
output describe what each check verifies, not the verdict; every
`Status:` for those checks is SUCCESS.
The real problem: `unwind=8` was insufficient for the 9-byte header
iterator, the 11-byte tokens iterator, and especially the 64-byte
`emit_len`/`contains` scan loops. CBMC needs `loop_bound + 1` unwinds.
Fix: bump the codegen harness `#[kani::unwind]` to 65 and pull the
buffer size into a named constant `BUF_SIZE` so the relationship
`UNWIND_N = BUF_SIZE + 1` is documented. This follows the existing
`kani_solver.rs` guidance ("If harnesses fail with unwinding assertion
violation, raise UNWIND_N rather than the loop bound"). The proof
obligations (header presence, task-ID containment, processor-ID
containment) are unchanged — only the unwinder gets enough budget to
fully explore the bounded loops.
No production code changes. The solver harnesses already pass at
unwind=8 and are untouched.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
force-pushed
the
fix/136-kani-harnesses
branch
from
bf157b3 to
dd0e88c
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
kanijob withcontinue-on-error: true(first-pass bounds)proof_link:fieldsHarnesses
kani_schedule_implies_no_deadline_missRMBound.lean:49(rmBound_ge_ln2) +RMBound.lean:76(rm_single_task)kani_priority_monotonicityRTA.lean:74(rtaStep_mono) +RTA.lean:65(totalInterference_mono)kani_zero_laxity_handledEDF.lean:88(edf_two_tasks_demand) +RMBound.lean:38(rmBound_one)kani_emit_preserves_scheduleRTA.lean:186(rta_finds_least_fixed_point)Design note
la_arena::Idxis opaque to Kani's symbolic execution — production typesThreadConstraint/SystemInstancecannot be symbolically constructed. Per task constraint (no production-source changes), harnesses verify the same mathematical invariants using local pure-function mirrors that match production to 6 decimal places (numeric constants derive fromrma_utilization_bound(n)inspar-analysis/scheduling.rs:522).Local verification
cargo build --tests -p spar-solver -p spar-codegenPASS (Kani files are empty modules under default cfg)cargo clippy --workspace --all-targets -- -D warningsPASScargo fmt --all -- --checkPASScargo test -p spar-solver -p spar-codegen --testsPASS (existing tests; Kani files report 0 tests as expected)rivet validatePASS (91 warnings, no new errors)cargo kani --testsnot run locally (sandbox blocked) — CI is the verifierWhy
continue-on-error: trueInitial unwind bounds may need tuning per harness; we collect data first, then hard-gate in a follow-up. Plan documented in workflow comment.
Test plan
kaniCI job runs (success preferred but non-blocking)🤖 Generated with Claude Code